ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), k:Knd, test:(decl-state(ds)ma-valtype(da; k)).
ecl-base-tuple(k; test)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions	t  T, x:A. B(x), ma-valtype(da; k), guard(T), P  Q, sq_type(T), Knd, prop{i:l}, decl-state(ds), , bor(p; q), P  Q, P  Q, b, A, b, Unit, (x  l), band(p; q), , , ff, (i = j), ecl-base-tuple(k; test), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), fpf(A; a.B(a)), eq_knd(a; b)
Lemmas	fpf wf, Id wf, eq int wf, bfalse wf, nat wf, nat plus wf, band wf, l member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, eq knd wf, assert-eq-knd, bor wf, bool wf, decl-state wf, Knd wf, Knd sq, subtype rel self, ma-valtype wf